package typesys;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import util.Pair;

import flowlogic.STSimplifier;

import ast.AtomicLabel;
import ast.CstPr;
import ast.Endorse;
import ast.FunApp;
import ast.Function;
import ast.Label;
import ast.LabelConjunction;
import ast.LabelDisjunction;
import ast.Principal;
import ast.Site;
import ast.Term;
import ast.TermVar;

public class RhoEval {
	
	public static HashSet<Term> eval(Term t, HashMap<String, HashSet<Term>> rho) 
			throws FunctionUndefinedException
	{
		HashSet<Term> result = new HashSet<Term>();
		
		if (t instanceof TermVar) {
			
			String name = ((TermVar) t).getName();
			if (STSimplifier.getChannelMap().containsKey(name)) {
				result.add(STSimplifier.getChannelMap().get(name));
			} else if (STSimplifier.getSites().contains(name)) {
				result.add(new Site(name));
			} else if (STSimplifier.getPrincipals().contains(name)) {
				// there is no need for the maintenance of acts-for
				// since eventually a channel constant is expected to be returned
				result.add(new Principal(name));
			} else if (name.equals("*")) {
				result.add(TopPrincipal.getInstance());
			} else if (name.equals("_")) {
				result.add(BottomPrincipal.getInstance());
			} else { // t is really a term variable
				result.addAll(rho.get(name));
			}
			
		} else if (t instanceof FunApp) {
			
			Function func = STSimplifier.getFunctionMap().get(((FunApp) t).getName());
			
			ArrayList<Term> argList = ((FunApp) t).getArgList();
			int arity = argList.size();
			ArrayList<ArrayList<Term>> resLists = new ArrayList<ArrayList<Term>>(arity);
			for (int i = 0; i < arity; i++) {
				resLists.add(new ArrayList<Term>());
				resLists.get(i).addAll(RhoEval.eval(argList.get(i), rho));
			}
			
			int[] indices = new int[arity];	
			boolean full = false;
			
			do {
				ArrayList<String> strArgList = new ArrayList<String>();
				for (int i = 0; i < arity; i++) {
					Term t1 = resLists.get(i).get(indices[i]);
					assert (t1 instanceof CstPr); // no endorsement allowed as function arguments
					strArgList.add(((CstPr) t1).getName());
				}
				
				String strAppRes = null;
				for (Pair<ArrayList<String>, String> row : func.getDefinition()) {
					if (strArgList.equals(row.getFst())) {
						strAppRes = row.getSnd();
						break;
					}
				}
				if (strAppRes == null) {
					throw new FunctionUndefinedException();
				}
				if (STSimplifier.getChannelMap().containsKey(strAppRes)) {
					result.add(STSimplifier.getChannelMap().get(strAppRes));
				} else if (STSimplifier.getSites().contains(strAppRes)) {
					result.add(new Site(strAppRes));
				} else if (STSimplifier.getPrincipals().contains(strAppRes)) {
					result.add(new Principal(strAppRes));
				} else if (strAppRes.equals("*")) {
					result.add(TopPrincipal.getInstance());
				} else if (strAppRes.equals("_")) {
					result.add(BottomPrincipal.getInstance());
				}
				full = true;
				for (int i = 0; i < arity; i++) {
					if (indices[i] + 1 < resLists.get(i).size()) {
						indices[i]++;
						full = false;
						break;
					} else {
						indices[i] = 0;
					}
				}
			} while (!full);
			
		} else if (t instanceof Endorse) {
			
			HashSet<Term> innerRes = RhoEval.eval(((Endorse) t).getT(), rho);
			for (Term tInner : innerRes) {
				result.add(new Endorse(tInner, ((Endorse) t).getL1(), ((Endorse) t).getL2()));
			}
		}
		
		return result;
	}
	
	private static int trmCounter = 0;
	
	public static HashSet<Label> eval(Label label, HashMap<String, HashSet<Term>> rho) 
			throws FunctionUndefinedException
	{
		HashSet<Label> result = new HashSet<Label>();
		
		ArrayList<ArrayList<Term>> termResults = new ArrayList<ArrayList<Term>>(); 
		getListOfTermResults(label, termResults, rho);
 		
		int[] indices = new int[termResults.size()];
		boolean full = true;
		do {
			trmCounter = 0;
			result.add(buildLabel(label, indices, termResults));
			for (int i = 0; i < indices.length; i++) {
				if (indices[i] + 1 < termResults.get(i).size()) {
					indices[i]++;
					full = false;
					break;
				} else {
					indices[i] = 0;
				}
			}
		} while (!full);
		
		return result;
	}
	
	private static Label buildLabel(
			Label oldLabel, 
			int[] indices, 
			ArrayList<ArrayList<Term>> trmResults) 
	{
		Label result = null;
		
		if (oldLabel instanceof LabelConjunction) {
			
			ArrayList<Label> lbs = new ArrayList<Label>();
			for (Label lb : ((LabelConjunction) oldLabel).getOps()) {
				lbs.add(buildLabel(lb, indices, trmResults));
			}
			result = new LabelConjunction(lbs);
			
		} else if (oldLabel instanceof LabelDisjunction) {
			
			ArrayList<Label> lbs = new ArrayList<Label>();
			for (Label lb : ((LabelDisjunction) oldLabel).getOps()) {
				lbs.add(buildLabel(lb, indices, trmResults));
			}
			result = new LabelDisjunction(lbs);
			
		} else {
			
			Principal o = (Principal) 
					(trmResults.get(trmCounter).get(indices[trmCounter]));
			trmCounter++;
			ArrayList<Term> ps = new ArrayList<Term>();
			for (int i = 0; i < ((AtomicLabel) oldLabel).getInfluencers().size(); i++) {
				ps.add((Principal) trmResults.get(trmCounter).get(indices[trmCounter]));
				trmCounter++;
			}
			result = new AtomicLabel(o, ps);
		}
		
		return result;
	}
	
	private static void getListOfTermResults(
			Label label, 
			ArrayList<ArrayList<Term>> res, 
			HashMap<String, HashSet<Term>> rho) throws FunctionUndefinedException
	{
		if (label instanceof LabelConjunction) {
			for (Label lb : ((LabelConjunction) label).getOps()) {
				getListOfTermResults(lb, res, rho);
			}
		} else if (label instanceof LabelDisjunction) {
			for (Label lb : ((LabelDisjunction) label).getOps()) {
				getListOfTermResults(lb, res, rho);
			}
		} else {
			AtomicLabel alb = (AtomicLabel) label;
			res.add(new ArrayList<Term>());
			res.get(res.size() - 1).addAll(RhoEval.eval(alb.getOwner(), rho));
			for (Term pTrm : alb.getInfluencers()) {
				res.add(new ArrayList<Term>());
				res.get(res.size() - 1).addAll(RhoEval.eval(pTrm, rho));
			}
		}
	}

}
